% !Mode:: "TeX:UTF-8"
\newcommand{\LcurrentBody}{
Пусть $L_0$ -- множество ключей, расположенных в некотором регионе таблицы перед исполнением инструкций тестового шаблона, $x_1$, $x_2$, ..., $x_n$ -- последовательность ключей того же региона, по которым происходят обращения с промахами в том же порядке, что и в тестовом шаблоне, $x'_1, x'_2, ..., x'_n$ -- последовательность ключей, вытесняемых обращениями к $x_1$, $x_2$, ..., $x_n$. Тогда $L$ -- выражение для множества ключей таблицы того же региона после этих обращений имеет вид:
$$L \equiv L_0 \setminus \bigcup_{i=1}^n \{x'_i\} \cup \bigcup_{i=1}^n (
\{x_i\} \setminus \cup_{j~=~i+1}^n \{x'_j\}).$$
}

\newcommand{\HitMissEquations}{
Пусть $L_0$ -- множество ключей, расположенных в таблице в некотором регионе перед исполнением инструкций тестового шаблона, $x_1, x_2, ..., x_n$ -- последовательность ключей того же региона, по которым происходят обращения с промахами в том же порядке, что и в
тестовом шаблоне, $x'_1$, $x'_2$, ..., $x'_n$ -- последовательность ключей, вытесняемых обращениями к $x_1$, $x_2$, ..., $x_n$. Тогда для обращения после этих по ключу $x$ в тот же регион справедливы следующие уравнения:
\begin{itemize}
\item для обращения с попаданием:
$$
\left[
   \begin{array}{l}
    x \in L_0 \wedge x \notin \{x'_1, x'_2, ..., x'_n\} \\
    x = x_1 \wedge x \notin \{x'_2, ..., x'_n\} \\
    x = x_2 \wedge x \notin \{x'_3, ..., x'_n\} \\
    ...\\
    x = x_{n-1} \wedge x \notin \{x'_n\} \\
    x = x_n \\
   \end{array}
  \right.
$$

\item для обращения с промахом ($x'$ --- вытесняемый ключ):
$$
\left\{
   \begin{array}{l}

  \left[
   \begin{array}{l}
    x \notin L_0 \wedge x \notin \{x_1, x_2, ..., x_n\} \\
    x = x'_1 \wedge x \notin \{x_2, ..., x_n\} \\
    x = x'_2 \wedge x \notin \{x_3, ..., x_n\} \\
    ...\\
    x = x'_{n-1} \wedge x \notin \{x_n\} \\
    x = x'_n \\
   \end{array}
  \right. \\

  { }\\

  \left[
   \begin{array}{l}
    x' \in L_0 \wedge x \notin \{x'_1, x'_2, ..., x'_n\} \\
    x' = x_1 \wedge x \notin \{x'_2, ..., x'_n\} \\
    x' = x_2 \wedge x \notin \{x'_3, ..., x'_n\} \\
    ...\\
    x' = x_{n-1} \wedge x \notin \{x'_n\} \\
    x' = x_n \\
   \end{array}
  \right. \\

  { }\\

  displaced(x')\\

%  { }\\
%
%  R(x) = R(x')\\
%
  \end{array}
\right.
$$

\end{itemize}
}

\newcommand{\CorrectnessMirror}{
%Если тестовый шаблон является совместным (т.е. для него существует хотя бы одна тестовая программа), то тестовая программа (инициализация плюс инструкции тестового шаблона), построенная по предлагаемому методу, соответствует тестовому шаблону.
Если построенная для последовательности обращений в таблицу $(S_1, k_1, R_1)$, $(S_2, k_2, R_2)$, ..., $(S_n, k_n, R_n)$ c дополнительным предикатом $P(k_1,$ $k_2, ..., k_n, R_1, R_2, ..., R_n)$ система ограничений является совместной, то ее решение $t_1, t_2, ..., t_m$, $r_1$, $r_2$, ..., $r_m$, $k_1, k_2, ..., k_n$, $R_1, R_2, ..., R_n$, удовлетворяет последовательности $S_1, ..., S_n$ и $P$ при любом начальном состоянии таблицы.
}

\newcommand{\FullnessMirror}{
Если при данном начальном состоянии таблицы со стратегией вытеснения не \texttt{none} для последовательности обращений в нее $(S_1, k_1, R_1)$, $(S_2, k_2, R_2)$, ..., $(S_n, k_n, R_n)$ c дополнительным предикатом $P(k_1$, $k_2, ..., k_n, R_1$, $R_2, ..., R_n)$ существует удовлетворяющая ей последовательность ключей, то система ограничений согласно соответствующему алгоритму
%из раздела~\ref{sec:constraints_generation_section}
будет совместной, если стратегия вытеснения является <<существенно вытесняющей>>.
}

\newcommand{\FullnessMirrorNone}{
Если при данном начальном состоянии таблицы со стратегией вытеснения \texttt{none} для последовательности обращений в нее $(S_1, k_1, R_1)$, $(S_2, k_2, R_2)$, ..., $(S_n, k_n, R_n)$ c дополнительным предикатом $P(k_1, k_2, ..., k_n, R_1$, $R_2, ..., R_n)$ существует удовлетворяющая ей последовательность ключей, то система ограничений согласно соответствующему алгоритму
%из раздела~\ref{sec:constraints_generation_section}
 будет совместной.
}

\newcommand{\PseudoLRUEssential}{
Стратегия вытеснения \PseudoLRU является существенно вытесняющей.
}

\newcommand{\UpperBoundLRUMirror}{
В условиях теоремы~\ref{mirror_fullness} для стратегии вытеснения \LRU достаточно использовать $m$ такое, что
  $$m \leqslant n \cdot w + M$$
  где $M$ -- количество элементов последовательности $S_1, S_2, ..., S_n$, равных miss.}

\newcommand{\PseudoLRUInvariant}{
Пусть ($\alpha_1~\alpha_2~\dots~\alpha_W$)
--- \PseudoLRU-ветвь некоторой позиции $i$. Тогда изменение этой
ветви согласно стратегии вытеснения \PseudoLRU определяется только
относительной позицией (относительно $i$) и происходит следующим
образом при обращении к ключу с (абсолютной) позицией $j$: если
$\pi^i_j \in [\frac{w}{2^k},~\frac{w}{2^{k-1}})$ для некоторого
$k=1,2,\dots,W$, то происходит изменение $\alpha_1 := 0,~\alpha_2 :=
0,~\dots,~ \alpha_{k-1} := 0,~\alpha_k := 1$; если $\pi^i_j = 0$, то
происходит изменение $\alpha_1 := 0,~\alpha_2 := 0,~\dots,~\alpha_W
:= 0$; вытеснение ключа на позиции $i$ происходит в том случае, когда
$\alpha_1 = 1~\wedge~\alpha_2 = 1~\wedge~\dots~\wedge~\alpha_W = 1$.
}

%\newcommand{\DiapazonLRU}{
%Решение системы (ключ $x'$)
%$$
%\left\{
%   \begin{array}{l}
%    x' = y \\
%    R(y) \cap (L \setminus \{x_1, x_2, ..., x_n\} ) = \{y\}\\
%   \end{array}
%  \right.
%$$
%где последовательность ключей $y, x_1, x_2, ..., x_n$ -- диапазон
%вытеснения, а $L$ -- множество ключей в таблице перед концом
%диапазона, является вытесняемым ключом для стратегии вытеснения \LRU
%согласно определению на перестановках.
%}
%
%\newcommand{\DiapazonFIFO}{
%Решение системы (ключ $y'$)
%$$
%\left\{
%   \begin{array}{l}
%    y' = y \\
%    R(y) \cap (L \setminus \{y_1, y_2, ..., y_n\} ) = \{y\}\\
%   \end{array}
%  \right.
%$$
%где последовательность ключей $y, y_1, y_2, ..., y_n$ -- диапазон
%вытеснения, является вытесняемым ключом для стратегии вытеснения
%\FIFO согласно определению на перестановках.
%}
%
%\newcommand{\MaxUpperBoundLRU}{
%$$0 \leqslant k \leqslant n \cdot w_1$$
%$$0 \leqslant h \leqslant n \cdot (w_1 + w_2 + 2)$$
%где $w_1$ -- ассоциативность кэш-памяти первого уровня, $w_2$ --
%ассоциативность кэш-памяти второго уровня, $n$ -- количество
%инструкций тестового шаблона.
%}

\newcommand{\LRUusefuls}{
Пусть $(t_1, r_1)$, $(t_2,r_2),$ ..., $(t_m,r_m)$ -- ключи и регионы инициализирующих обращений, $(k_i, R_i)$ -- ключ и регион обращения, для которого описывается вытеснение (будем его называть <<вытесняемым>>), причем $(k_i||R_i) \in \{(t_1||r_1)$, ..., $(t_m||r_m)$, $(k_1||R_1)$, ..., $(k_{i-1}||R_{i-1})\}$ и $\{(t_1||r_1), ...,(t_m||r_m)\}$ --- все разные. Тогда $k_i$ не вытеснен из региона $R_i$ согласно определению \LRU на перестановках тогда и только тогда, когда $$\sum\limits_{j=1}^{m+n} [u_{k_i,R_i}(s_j)] < w$$
где последовательность $s \equiv \langle (t_1||r_1), ..., (t_m||r_m), (k_1||R_1), ..., (k_n||R_n)\rangle$,\\$R(s_i)$~---~вторая компонента $s_i$ (регион), а формула полезного обращения такая:
$$u_{k_i,R_i}(s_j) \equiv ((k_i||R_i) \notin \{s_j, ..., s_{m+n}\} \wedge
R_i = R(s_j) \wedge s_j \notin\{s_{j+1},..., s_{m+n}\})$$
}

\newcommand{\PLRUusefuls}{
Пусть $(t_1, r_1)$, $(t_2,r_2),$ ..., $(t_m,r_m)$ -- ключи и регионы инициализирующих обращений, $(k_i, R_i)$ -- ключ и регион обращения, для которого описывается вытеснение (будем его называть <<вытесняемым>>), причем $(k_i||R_i) \in \{(t_1||r_1)$, ..., $(t_m||r_m)$, $(k_1||R_1)$, ..., $(k_{i-1}||R_{i-1})\}$ и $\{(t_1||r_1), ...,(t_m||r_m)\}$ --- все разные. Тогда $k$ не вытеснен из региона $R$ согласно определению на ветвях бинарного дерева тогда и только тогда, когда $$\sum\limits_{j=1}^{m+n} [u_{k_i,R_i, \pi'_i}(s_j)] < W$$
где последовательность $s \equiv \langle (t_1||r_1), ..., (t_m||r_m), (k_1||R_1), ..., (k_n||R_n)\rangle$,\\$R(s_i)$ --- вторая компонента $s_i$ (регион), а формула полезного обращения такая:
$$u_{k_i,R_i,\pi'_i} (s_j) \equiv \left\{\begin{array}{l}
(k_i||R_i) \notin \{s_j, s_{j+1}, ..., s_{m+n}\}\\
R_i = R(s_j)\\
(\pi'_i||R_i) \in \{(\pi_j||R_j), (\pi_{j+1}||R_{j+1}), ..., (\pi_{m+n}||R_{m+n})\}\\
\bigwedge\limits_{k = j+1}^{m+n} (R_j = R_k ~\wedge~(\pi'_i||R_i) \notin \{(\pi_j||R_j), (\pi_{j+1}||R_{j+1}), ..., (\pi_k||R_k)\}\\
\hspace{2cm} \rightarrow P(\pi_j \oplus \pi'_i, \pi_k \oplus \pi'_i))\\
\end{array}\right.
$$
$$P(x, y) \equiv (y > x~~\wedge~~x \oplus y > x)$$

$\pi'_i$ определено следующим образом: если $S_i$ = hit, то  
$$
\begin{array}{l}
\texttt{(ite~} ((k_i||R_i) = (k_{i-1}||R_{i-1})) ~~ (\pi'_i = \pi_{i-1})\\
\texttt{(ite~} ((k_i||R_i) = (k_{i-2}||R_{i-2})) ~~ (\pi'_i = \pi_{i-2})\\
... ~(\pi'_i = 0)\texttt{)))...)}\\
\end{array}
$$

если $S_i = $ miss, то ( $\{\pi_i, ..., \pi_j\}_m$ обозначает подмножество множества позиций от $i$'го до $j$'го обращения из неуспешных обращений):
$$
\begin{array}{l}
\texttt{(ite~} ((k_i||R_i) = (k_{i-1}||R_{i-1})) ~~ (\pi'_i = \pi_{i-1})\\
\texttt{(ite~} ((k_i||R_i) = (k_{i-2}||R_{i-2})) ~~ (\pi'_i = \pi_{i-2} \wedge \pi'_i \in \{\pi_{i-1}\}_m)\\
\texttt{(ite~} ((k_i||R_i) = (k_{i-3}||R_{i-3})) ~~ (\pi'_i = \pi_{i-3} \wedge \pi'_i \in \{\pi_{i-1}, \pi_{i-2}\}_m)\\
... ~(\pi'_i = 0)\texttt{)))...)}\\
\end{array}
$$
} 